Refinements are always about the read property, so refine just that part. If I recall correctly, this was Property::rw because this was implemented before read/write properties was. Time to fix that.

This resolves these issues:

• 1651
• 1566
• 1486

The comments associated seems to imply that refinements on just the read property would cause read and write types to be completely disjoint, and I don't believe that to be a possibility. Refinements inherently restricts the domain, not transform it completely in a way that causes the disjointedness. At this point I would have looked at the git log for more information, but alas. Making the change seems to have had no effects on the tests.

In the unit test, that last reference of x should really be (in non-normalized terms) of type Foo & { read p: ~true } & { write p: true <: 'a <: boolean }. Whenever there are two intersecting tables whose read and write property are not shared, replace it by the join and meet of the read's lower bound and write's upper bound, following the usual polarity laws. After solving for 'a (suppose 'a ~ boolean) we can expand our previous type Foo & { read p: ~true, write p: unknown } & { read p: never, write p: boolean }. Performing the rewrite rule, you get Foo & { read p: ~true | boolean, write p: unknown & boolean }. Since write p: unknown & boolean is already a part of Foo, this field is redundant, and likewise with read p: ~true | boolean, so the entire type refinement for x would have been invalidated simply by intersecting the lvalues if an improvement was made to typestates.

It's not enough to update ConstraintGenerator alone to fix the lvalues' types just based on the strong updates that is obvious in the syntax, I think you will also have to update DataFlowGraph to create new definitions for each parameters passed into functions, and then use union-find to unify two DefId as the same during constraint resolution. This should solve the issue with whether this snippet shares the same definition:

local x = 5 -- x1
function f(y)
  y += 2
end
f(x) -- x2

In the first pass, we want to assume the worst-case scenario by generating as many definitions as possible, and only in the second pass during constraint resolution are we able to gather enough information to unify definitions together according to the potential effects a function may have, e.g. the write fields or upvalue mutation, etc.. This turns the problem into a join semilattice. By this point, x1 and x2 are considered the same definition as per union-find. The type graph will need to have some DefId carrier somewhere plus some way to canonicalize them to the canonical definition.